incr(nil) → nil
incr(cons(X, L)) → cons(s(X), incr(L))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, adx(L)))
nats → adx(zeros)
zeros → cons(0, zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → L
↳ QTRS
↳ DependencyPairsProof
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), incr(L))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, adx(L)))
nats → adx(zeros)
zeros → cons(0, zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → L
ZEROS → ZEROS
ADX(cons(X, L)) → ADX(L)
NATS → ZEROS
ADX(cons(X, L)) → INCR(cons(X, adx(L)))
NATS → ADX(zeros)
INCR(cons(X, L)) → INCR(L)
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), incr(L))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, adx(L)))
nats → adx(zeros)
zeros → cons(0, zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → L
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
ZEROS → ZEROS
ADX(cons(X, L)) → ADX(L)
NATS → ZEROS
ADX(cons(X, L)) → INCR(cons(X, adx(L)))
NATS → ADX(zeros)
INCR(cons(X, L)) → INCR(L)
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), incr(L))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, adx(L)))
nats → adx(zeros)
zeros → cons(0, zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → L
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
ZEROS → ZEROS
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), incr(L))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, adx(L)))
nats → adx(zeros)
zeros → cons(0, zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → L
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
INCR(cons(X, L)) → INCR(L)
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), incr(L))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, adx(L)))
nats → adx(zeros)
zeros → cons(0, zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → L
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
INCR(cons(X, L)) → INCR(L)
The value of delta used in the strict ordering is 8.
POL(cons(x1, x2)) = 2 + (4)x_2
POL(INCR(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), incr(L))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, adx(L)))
nats → adx(zeros)
zeros → cons(0, zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → L
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
ADX(cons(X, L)) → ADX(L)
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), incr(L))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, adx(L)))
nats → adx(zeros)
zeros → cons(0, zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → L
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ADX(cons(X, L)) → ADX(L)
The value of delta used in the strict ordering is 1.
POL(cons(x1, x2)) = 1/4 + (4)x_2
POL(ADX(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), incr(L))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, adx(L)))
nats → adx(zeros)
zeros → cons(0, zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → L